A:Type, es:ES, I:AbsInterface(A), P:(E), p:(e:E. Dec(P(e))), e:E.
((e  (I|p)))  ((I|p)(e) ~ I(e)) 

latex

Definitions	False, t  T, x:A. B(x), P  Q, b, Top, isl(x), left + right, P  Q, x:AB(x), , E, s ~ t, Type, ES, do-apply(f;x), can-apply(f;x), f o g  , p-filter(f), p-restrict(f;p), X(e), (I|p), e  X, AbsInterface(A), f(a), x(s), Dec(P), s = t
Lemmas	assert wf, isl wf, false wf